$\forall$$x$:Id, $T$:Type. Normal($T$) $\Rightarrow$ Normal($x$ : $T$)